$\forall$$A$:Type, $d_{1}$,$d_{2}$,$d_{3}$,$d_{4}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $f$,$g$:fpf($A$; $a$.$B$($a$)), $x$:$A$, $z$:$B$($x$).
\\[0ex]fpf{-}sub($A$; $a$.$B$($a$); $d_{4}$; $f$; $g$)
\\[0ex]$\Rightarrow$ ($\uparrow$fpf{-}dom($d_{3}$; $x$; $f$))
\\[0ex]$\Rightarrow$ (fpf{-}cap($f$; $d_{1}$; $x$; $z$) = fpf{-}cap($g$; $d_{2}$; $x$; $z$) $\in$ $B$($x$))